(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
f(x, c(x), c(y)) → f(y, y, f(y, x, y))
f(s(x), y, z) → f(x, s(c(y)), c(z))
f(c(x), x, y) → c(y)
g(x, y) → x
g(x, y) → y
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1
Tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5
S tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F, G
Compound Symbols:
c1, c2, c3, c4, c5
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
G(z0, z1) → c5
G(z0, z1) → c4
F(c(z0), z0, z1) → c3
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1
Tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
S tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
(5) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
g(z0, z1) → z0
g(z0, z1) → z1
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
S tuples:
F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
z0,
c(
z0),
c(
z1)) →
c1(
F(
z1,
z1,
f(
z1,
z0,
z1)),
F(
z1,
z0,
z1)) by
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1
(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1
(11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c1
(13) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c3
(15) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c3
(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
We considered the (Usable) Rules:none
And the Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F(x1, x2, x3)) = [2]x2
POL(c(x1)) = [1] + x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(f(x1, x2, x3)) = 0
POL(s(x1)) = 0
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c3
(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
s(
z0),
z1,
z2) →
c2(
F(
z0,
s(
c(
z1)),
c(
z2))) by
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
S tuples:
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c3, c2
(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
z1,
c(
z1),
c(
s(
z0))) →
c3(
F(
s(
z0),
s(
z0),
f(
z0,
s(
c(
z1)),
c(
s(
z0))))) by
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))
S tuples:
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c3, c2
(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
S tuples:
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c3, c2
(25) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
z1,
c(
z1),
c(
s(
z0))) →
c3(
F(
s(
z0),
z1,
s(
z0))) by
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
S tuples:
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c3
(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
c(
c(
z1)),
c(
c(
c(
z1))),
c(
c(
z1))) →
c1(
F(
c(
z1),
c(
c(
z1)),
c(
z1))) by
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
(28) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
S tuples:
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c3, c1
(29) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
s(
s(
y0)),
z1,
z2) →
c2(
F(
s(
y0),
s(
c(
z1)),
c(
z2))) by
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
(30) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
S tuples:
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
K tuples:
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c3, c1, c2
(31) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
(32) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
S tuples:
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
K tuples:
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c3, c1, c2
(33) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
x0,
c(
x0),
c(
s(
s(
z0)))) →
c3(
F(
s(
s(
z0)),
s(
s(
z0)),
f(
z0,
s(
c(
s(
c(
x0)))),
c(
c(
s(
s(
z0))))))) by
F(c(s(s(x0))), c(c(s(s(x0)))), c(s(s(x0)))) → c3(F(s(s(x0)), s(s(x0)), f(x0, s(c(s(c(c(s(s(x0))))))), c(c(s(s(x0)))))))
(34) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(x0))), c(c(s(s(x0)))), c(s(s(x0)))) → c3(F(s(s(x0)), s(s(x0)), f(x0, s(c(s(c(c(s(s(x0))))))), c(c(s(s(x0)))))))
S tuples:
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
K tuples:
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c3, c1, c2
(35) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
We considered the (Usable) Rules:none
And the Tuples:
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(x0))), c(c(s(s(x0)))), c(s(s(x0)))) → c3(F(s(s(x0)), s(s(x0)), f(x0, s(c(s(c(c(s(s(x0))))))), c(c(s(s(x0)))))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F(x1, x2, x3)) = [2]x1 + x2
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(f(x1, x2, x3)) = 0
POL(s(x1)) = [1] + x1
(36) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(x0))), c(c(s(s(x0)))), c(s(s(x0)))) → c3(F(s(s(x0)), s(s(x0)), f(x0, s(c(s(c(c(s(s(x0))))))), c(c(s(s(x0)))))))
S tuples:none
K tuples:
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c3, c1, c2
(37) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(38) BOUNDS(1, 1)